Inference at * 1 0 
Iof proof for Lemma all functionality wrt implies:



1. S : Type
2. T : Type
3. P : S
4. Q : S
5. S = T
6. z:S. P(z)  Q(z)
7. x:S. P(x)
8. y : T
  Q(y) 

latex

 by PERMUTE{1:n, 1:n} 

latex

 1: .....wf..... NILNIL

 1:   y  S
 .

Definitions

t  T, f(a), x(s), s = t, , x:AB(x), Type, P  Q, x:A. B(x)